Inference at * 1 1 1 2 2 1 
Iof proof for Lemma decidable implies better:



1. P : 
2. Q : x:P.
3. P
4. Q
5. Q  
6. P  Q
  False 

latex

 by D (-1) THEN Auto 

latex

 .

Definitions

A, P  Q, False